T:Type, as,as',bs,cs:(T List).
(||as|| = ||as'||  )  (append(as; cs) = append(as'; bs)  (T List))  (cs = bs) 

latex

Definitions	P  Q, t  T, x:A. B(x), ||as||, P  Q, guard(T), P  Q, prop{i:l}, append(as; bs)
Lemmas	append wf, general-append-cancellation, length wf1